signature Thm =
sig
  include FinalThm
end
